es:ES, e:E, x:Id. first(e)  ((x when e) ~ x initially@loc(e) ) 

latex

Definitions	s.x, False, P  Q, A, t  T, x:A. B(x), b, b, , s = t, Prop, first(e), x:AB(x), x:AB(x), P & Q, P  Q, Unit, left+right, (state when e), x initially@i , x when e, ES, E, Id
Lemmas	Id wf, es-E wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf